COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR X Y Z ε SEXP
C00003 00003	AXIOM CONS:
C00004 00004	AXIOM APPEND:
C00005 ENDMK
C⊗;
DECLARE INDVAR X Y Z ε SEXP;
DECLARE INDVAR U V W ε LIST;
DECLARE OPCONST CAR(LIST) = SEXP[R←700];
DECLARE OPCONST CDR(LIST) = LIST[R←700];
DECLARE OPCONST CONS(SEXP,LIST) = LIST;
DECLARE PREDCONST NULL 1 [R←700];
DECLARE OPCONST *(LIST,LIST) = LIST [INF];

DECLARE PREDPAR P 1;

DECLARE INDCONST NILLεLIST;

DECLARE OPCONST REVERSE(LIST) = LIST[R←700];
DECLARE OPCONST REV1(LIST,LIST) = LIST;
AXIOM CONS:
	∀X U.(CAR CONS(X,U) = X)
	∀X U.(CDR CONS(X,U) = U)
	∀U.(¬NULL U ⊃ CONS(CAR U,CDR U) = U)
	∀X U.¬NULL CONS(X,U)
;;

AXIOM INDUCTION:
	∀U.(NULL U ∨ P(CDR U) ⊃ P(U)) ⊃ ∀U.P(U)
;;


AXIOM NULL:
	∀U.(NULL U ≡ U = NILL)
;;
AXIOM APPEND:
	∀U V.(U * V = IF NULL U THEN V ELSE CONS(CAR U, CDR U * V))
;;

AXIOM REVERSE:
	∀U.(REVERSE U = REV1(U,NILL))
	∀U V.(REV1(U,V) = IF NULL U THEN V ELSE REV1(CDR U,CONS(CAR U,V)))
;;